open util/boolean

///////////////////////////
/// SIGNATURES
//////////////////////////

sig Location { }

sig Event {
	location: lone Location,
	public: Bool
}

sig User {
	calendar: one Calendar
}

sig Calendar {
	events: set Event
}

sig Invitation {
	event: one Event,
	sender: one User,
	receiver: one User
}

sig DetailVisibility {
	event: one Event,
	users: set User
}

///////////////////////////
/// FUNCTIONS
//////////////////////////

//returns the owner of an event
fun eventOwner[e: Event]: one User {
	(User<:calendar).(Calendar<:events).e
}

// returns the set of Invitee of the given event
fun eventInvitedGuests[e: Event]: set User {
	(Invitation<:event).e.receiver
}

///////////////////////////
/// FACTS
//////////////////////////

fact calendarProperties {
	// (1) Each calendar must belong to one and only one user
	all c: Calendar | one u: User | u.calendar = c
}

fact eventProperties {
	// (1) Each event must belong to one and only one calendar
	all e: Event | one c: Calendar | e in c.events
	// (3) Each event must have its own detailvisibility
	all e: Event | one d: DetailVisibility | d.event = e
}

fact invitationProperties {
	// (1) The owner of the event can't be invited to his own event
	all i: Invitation | eventOwner[i.event] != i.receiver
	// (2) Each user has at most one invitation per event
	no disj i1, i2: Invitation | i1.event = i2.event && i1.receiver = i2.receiver
	// (3) An invitation to one event can be performed only by its owner
	all i: Invitation | i.sender = eventOwner[i.event]
}

fact visibilityProperties {
	// (1) Access control policy
	all d: DetailVisibility | let e = d.event | (
		// (1.1) If an event is public all users see its details
		e.public = True implies (d.users = User) else
		// (1.2) If an event is private and doesn't have any guests only 
		// the owner sees details (eventInvitedGuests[e] = empty)
		// (1.3) If an event is shared owner and participants see 
		// details (eventInvitedGuests[e] != empty)
		d.users = eventOwner[e] + eventInvitedGuests[e]
	)
}

///////////////////////////
/// ASSERTIONS
//////////////////////////

assert noEventBelongingToMultipleCalendar {
	no disj c1, c2: Calendar | (c1.events & c2.events) != none
}

check noEventBelongingToMultipleCalendar

assert noMultipleDetailVisibilitiesReferringToTheSameEvent {
	no disj d1, d2: DetailVisibility  | (d1.event & d2.event) != none
}

check noMultipleDetailVisibilitiesReferringToTheSameEvent

assert noTwoUsersOwningTheSameCalendar {
	no disj u1, u2: User | u1.calendar = u2.calendar
}

check noTwoUsersOwningTheSameCalendar 

assert noSelfInvitationToOneEvent {
	no i: Invitation | i.sender = i.receiver
}

check noSelfInvitationToOneEvent

assert noInvitationPerformedToSomeoneElsesEvent {
	no i: Invitation | one e: Event | i.event = e && i.sender != eventOwner[e]
}

check noInvitationPerformedToSomeoneElsesEvent

assert noVisibilityForNonInvitedUsersForPrivateEvent {
	no d: DetailVisibility | one u: User | 
		d.event.public = False && u != eventOwner[d.event] && 
		u not in eventInvitedGuests[d.event] && u in d.users
}

check noVisibilityForNonInvitedUsersForPrivateEvent

assert noMultipleVisibilityForSameEvent {
	no disj d1, d2: DetailVisibility | d1.event = d2.event
}

check noMultipleVisibilityForSameEvent

///////////////////////////
/// PREDICATES
//////////////////////////

pred showInvitations[e: Event] {
	#Event = 1
	#User = 3
	#Location = 0
	#Invitation = 1
	e.public = False
}

run showInvitations for 5

pred showAccessControlPolicyForPrivateEvent[e: Event] {
	#User = 5
	#Event = 1
	#Invitation = 2
	e.public = False
}

run showAccessControlPolicyForPrivateEvent for 5 but 0 Location, 1 Event

pred showAccessControlPolicyForPublicEvent[e: Event] {
	#User = 3
	#Event = 1
	#Invitation = 0
	e.public = True
}

run showAccessControlPolicyForPublicEvent for 5

pred show {
	#Event > #Calendar
	#Location = #Calendar
}

run show for 5 but 4 Invitation

